First Isomorphism Theorem: G/ker(f) ≅ im(f)
The First Isomorphism Theorem states that for any group homomorphism f : G → H, the quotient group G/ker(f) is isomorphic to the image im(f): G/ker(f) ≅ im(f). The proof constructs an explicit map from the quotient to the image using the universal property of quotients, then proves it's bijective: injective (if f(x) = f(y) then [x] = [y]) and surjective (every element of im(f) has a preimage). This theorem is fundamental in algebra, connecting quotient structures with image substructures and enabling the study of homomorphisms through their kernels.
Interactive Lean 4 proof — click a line to see its strategy and explanation inline
Strategy: Define the canonical homomorphism from G/ker(f) to im(f) that will become our isomorphism.
Explanation: Given a homomorphism f : G →* H, we construct a group homomorphism (→*) from the quotient G ⧸ ker(f) to the image im(f). This map will send each coset [g] ↦ f(g). The challenge is proving this is well-defined (independent of coset representative) and is a homomorphism. We'll use the universal property of quotient groups to lift a map from G to a map from G/ker(f).
Strategy: Enable classical logic for the proof.
Explanation: The classical tactic allows us to use the law of excluded middle and the axiom of choice. This is standard in Lean when working with quotients and decidability, as it simplifies many proofs by allowing us to make case distinctions freely.
Strategy: Define an auxiliary homomorphism φ : G → im(f) before lifting to the quotient.
Explanation: We define φ as a group homomorphism from G to image_subgroup f. The underlying function (toFun) sends each g ∈ G to the pair ⟨f g, proof⟩ where the proof is ⟨g, rfl⟩, witnessing that f(g) is indeed in the image (since f(g) = f(g) by reflexivity). The image_subgroup f is a subtype {h : H | ∃ g, f(g) = h}, so we must package f(g) with evidence of membership.
Strategy: Prove that φ preserves the identity: φ(1) = 1.
Explanation: To show φ is a homomorphism, we must verify map_one': φ(1_G) = 1_{im(f)}. We use ext (extensionality) to reduce this to showing the underlying elements are equal in H. Then simp applies the fact that f(1) = 1 (a property of all group homomorphisms) to complete the proof. This shows ⟨f(1), ...⟩ = ⟨1, ...⟩ in the image subgroup.
Strategy: Prove that φ preserves multiplication: φ(ab) = φ(a)φ(b).
Explanation: To complete the homomorphism structure, we prove map_mul'. Introduce arbitrary elements a, b ∈ G. Use ext to reduce to showing equality of underlying elements in H. Then simp with map_mul (which states f(ab) = f(a)f(b) for homomorphisms) completes the proof. This shows ⟨f(ab), ...⟩ = ⟨f(a), ...⟩ · ⟨f(b), ...⟩ = ⟨f(a)f(b), ...⟩. Now φ : G →* image_subgroup f is fully defined.
Strategy: Prove the kernel condition required by the universal property of quotients.
Explanation: To lift φ to a map from the quotient G/ker(f), we must verify that ker(f) ⊆ ker(φ). That is, for all x ∈ ker(f), we have φ(x) = 1 in im(f). This condition ensures the map is well-defined on cosets: if x and y are in the same coset (i.e., x⁻¹y ∈ ker(f)), then φ(x) = φ(y). This is the key property that allows us to invoke QuotientGroup.lift.
Strategy: Show that elements in ker(f) map to the identity under φ.
Explanation: Introduce x and the hypothesis hx : x ∈ ker(f). Use ext to reduce to showing the underlying elements in H are equal. Unfold the definitions: φ sends x ↦ ⟨f(x), ...⟩, kernel_subgroup f is {x : G | f(x) = 1}, and we need to show ⟨f(x), ...⟩ = ⟨1, ...⟩. The simp tactics expand these definitions and apply hx : f(x) = 1, completing the proof. This establishes hker, the crucial property for lifting.
Strategy: Apply the universal property to obtain the desired homomorphism G/ker(f) → im(f).
Explanation: QuotientGroup.lift is the universal property of quotient groups: given a homomorphism φ : G → H such that N ⊆ ker(φ), there exists a unique homomorphism G/N → H making the diagram commute. Here, N = ker(f), φ : G → im(f), and hker proves the kernel condition. The result is the homomorphism firstIsoMap : G/ker(f) →* im(f) defined by [g] ↦ f(g). This completes the definition of firstIsoMap.
Strategy: Prove that firstIsoMap is bijective (both injective and surjective).
Explanation: To establish the isomorphism, we must prove that firstIsoMap : G/ker(f) → im(f) is bijective. Function.Bijective is defined as the conjunction of injective and surjective. We'll prove each property separately: injectivity means if firstIsoMap([x]) = firstIsoMap([y]) then [x] = [y], and surjectivity means every element of im(f) has a preimage in G/ker(f).
Strategy: Split the goal into two parts: injective and surjective.
Explanation: The constructor tactic applies the constructor for the conjunction (AND). Since Function.Bijective f is defined as Injective f ∧ Surjective f, this splits our goal into two subgoals: first prove injectivity, then prove surjectivity. The · bullets will separate these two sub-proofs.
Strategy: Begin the injectivity proof by unfolding the definition and introducing elements.
Explanation: Unfold Function.Injective to its definition: ∀ x y, f(x) = f(y) → x = y. Introduce arbitrary elements x, y ∈ G/ker(f). The goal becomes: if firstIsoMap(x) = firstIsoMap(y), then x = y. To work with elements of the quotient, we'll use quotient induction to reduce to representatives in G.
Strategy: Use quotient induction to work with representatives.
Explanation: QuotientGroup.induction_on is the induction principle for quotients: to prove a property P([x]) for all cosets, it suffices to prove P([g]) for all representatives g ∈ G. We apply this twice: first to x, obtaining a representative x' ∈ G, then to y, obtaining y' ∈ G. Now we work with x = [x'] and y = [y'], which allows us to use the explicit definition of firstIsoMap on representatives.
Strategy: Simplify the goal using definitions and introduce the equality hypothesis.
Explanation: Simp unfolds: firstIsoMap applied to [x'] via lift_mk gives f(x'), homomorphism coercions, subtype extensionality (two elements ⟨a, p⟩ and ⟨b, q⟩ are equal iff a = b), and QuotientGroup.eq (which states [x'] = [y'] iff x'⁻¹y' ∈ ker(f)). After simplification, the goal becomes: if f(x') = f(y') (hypothesis h), then x'⁻¹y' ∈ ker(f). This is the heart of injectivity for the quotient map.
Strategy: Unfold the definition of kernel and apply homomorphism properties.
Explanation: Expand kernel_subgroup f to the set {x : G | f(x) = 1}, and unfold the subgroup membership predicates. Apply homomorphism properties: f(x'⁻¹y') = f(x'⁻¹)f(y') = f(x')⁻¹f(y') using map_mul and map_inv. The goal is now: prove f(x')⁻¹f(y') = 1, given h : f(x') = f(y'). This is a straightforward algebraic manipulation.
Strategy: Complete the injectivity proof by algebraic manipulation.
Explanation: Prove the intermediate fact h' : (f x')⁻¹ * (f y') = 1. Substitute h : f(x') = f(y') to get (f x')⁻¹ * (f x') = 1. The aesop tactic (automated proof search) solves this using group axioms: a⁻¹ * a = 1 for all a. Finally, exact h' provides this as the proof that x'⁻¹y' ∈ ker(f), establishing [x'] = [y']. This completes the injectivity proof.
Strategy: Begin the surjectivity proof by introducing an arbitrary element of the codomain.
Explanation: Surjectivity means ∀ y, ∃ x, f(x) = y. Introduce an arbitrary element x ∈ im(f). We must find a preimage in G/ker(f). Since x is in the image of f, by definition there exists some g ∈ G with f(g) = x. We'll use this witness to construct our preimage coset [g].
Strategy: Destructure the image element to extract a witness from G.
Explanation: The element x ∈ im(f) is a subtype: a pair ⟨x, proof⟩ where proof witnesses x ∈ {h : H | ∃ g, f(g) = h}. The rcases tactic destructures this: we get x (the underlying element of H) and ⟨g, rfl⟩ (the witness that f(g) = x). The rfl indicates that the equality f(g) = x is definitional (it's the way x was constructed). Now we have g ∈ G such that f(g) = x.
Strategy: Provide the coset [g] as the preimage and verify it maps to x.
Explanation: The use tactic provides the witness for the existential: we claim that [g] (denoted QuotientGroup.mk g) is the preimage of x. We must verify that firstIsoMap([g]) = x. By definition of firstIsoMap (via lift), firstIsoMap([g]) = f(g). Since we know f(g) = x (from the rcases step), the equality holds. The aesop tactic completes this verification automatically, closing the surjectivity proof and thus the bijectivity theorem.
Strategy: Package the bijective homomorphism as a group isomorphism.
Explanation: Define the First Isomorphism Theorem as a group isomorphism (≃*) from G ⧸ f.ker to f.range. We use MulEquiv.ofBijective, which constructs an isomorphism from a homomorphism and a proof of bijectivity. The homomorphism is firstIsoMap f, and the bijectivity proof is firstIsoMap_bijective f. The definition is noncomputable because it relies on classical logic (via the classical tactic used earlier). This completes the First Isomorphism Theorem: G/ker(f) ≅ im(f). □
💡 Tip: Click on any line above to see its strategy and explanation inline. Click again to hide it.
The proof constructs an explicit isomorphism via the universal property of quotients and establishes bijectivity:
Key insight: The First Isomorphism Theorem reveals that every homomorphism f : G → H factors through its kernel: G → G/ker(f) → im(f) → H. The middle map is an isomorphism, showing that the "essential content" of f is captured by the quotient structure. This is fundamental for understanding homomorphisms structurally rather than elementwise.
Universal property of quotient groups: if φ : G → H is a homomorphism with N ⊆ ker(φ), then φ lifts uniquely to a homomorphism G/N → H. This is the key principle that allows us to define maps from quotients by defining maps from the original group and verifying a kernel condition. Essential for constructing firstIsoMap.
Induction principle for quotients: to prove P([x]) for all cosets [x] ∈ G/N, it suffices to prove P([g]) for all representatives g ∈ G. This allows us to work with concrete elements rather than abstract cosets, simplifying proofs about quotient structures. Crucial for the injectivity proof where we need to manipulate representatives.
Characterization of equality in quotients: [x] = [y] in G/N if and only if x⁻¹y ∈ N. This is the fundamental property of quotient groups that translates coset equality into group membership. Used extensively in the injectivity proof to show that equal images imply equal cosets by verifying the difference lies in the kernel.
Constructor for group isomorphisms: a bijective group homomorphism is a group isomorphism. Given a homomorphism f : G →* H and a proof that f is bijective, this constructs the isomorphism G ≃* H with inverse. This packages our bijective firstIsoMap as the final isomorphism, completing the theorem statement.
The First Isomorphism Theorem is one of the fundamental isomorphism theorems in algebra, providing a canonical way to understand homomorphisms through their kernels. It reveals that every homomorphism can be "factored" into three steps: a quotient map (G → G/ker(f)), an isomorphism (G/ker(f) ≅ im(f)), and an inclusion (im(f) → H). This decomposition is powerful: it shows that the kernel completely determines the structure of the image, and that studying f reduces to studying the simpler quotient structure. Applications are ubiquitous: from proving that ℤ/nℤ ≅ ℤ_n to understanding normal subgroups, from linear algebra (rank-nullity theorem) to category theory (exact sequences). The theorem exemplifies the algebraic philosophy of understanding objects through their morphisms and quotients.